Nuprl Lemma : l_before-es-before-iff 11,40

the_es:event_system{i:l}, e,e',y:es-E(the_es).
l_before(e'y; before(e); es-E(the_es))  (es-locl(the_ese'y es-locl(the_esye)) 
latex


Definitionsevent_system{i:l}, t  T, x:AB(x), es-E(es), es-locl(esee'), prop{i:l}, P  Q, l_before(xylT), before(e), P  Q, P  Q, P  Q, b, , False, Unit, guard(T), xt(x), wellfounded{i:l}(Ax,y.R(x;y)), es-first(ese), b, A, (x  l), P  Q, es-pred(ese)
Lemmasl member wf, es-pred-locl, member singleton, l before append iff, es-pred wf, es-locl-wellfnd, es-locl-iff, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf, l before member, member-es-before, l before-es-before, l before wf, es-before wf, es-locl wf, es-E wf, event system wf

origin